package com.googlecode.kipler.transformations;

import java.util.ArrayList;
import java.util.Iterator;
import java.util.List;
import java.util.Set;

import com.googlecode.kipler.container.dl.ABox;
import com.googlecode.kipler.container.dl.Individual;
import com.googlecode.kipler.container.dl.operational.IndividualNameManager;
import com.googlecode.kipler.satisfiability.reasoner.UnsatisfiableException;
import com.googlecode.kipler.satisfiability.reasoner.profile.Logic;
import com.googlecode.kipler.satisfiability.reasoner.profile.ReasonerFactory;
import com.googlecode.kipler.syntax.concept.BooleanConcept;
import com.googlecode.kipler.syntax.concept.CardinalityRestriction;
import com.googlecode.kipler.syntax.concept.Concept;
import com.googlecode.kipler.syntax.concept.InequalityConstructor;
import com.googlecode.kipler.syntax.concept.Nominal;
import com.googlecode.kipler.syntax.concept.BooleanConcept.Constructor;
import com.googlecode.kipler.syntax.formula.ConceptAssertion;

public class CardinalityRestrictionsToABox {
	public ABox transform(Set<CardinalityRestriction> restrictions)
			throws UnsatisfiableException {
		ABox result = ReasonerFactory.getReasoner(Logic.SHOIQ).getProfile()
				.getWcsFactory().createWcs().createWorld().getABox();
		List<Concept> globalConcepts = new ArrayList<Concept>();
		for (CardinalityRestriction cr : restrictions) {
			if (cr.getConstructor() == InequalityConstructor.AT_MOST) {
				Concept globalConcept = addAtMost(result, cr);
				globalConcepts.add(globalConcept);
			}
			if (cr.getConstructor() == InequalityConstructor.AT_LEAST) {
				addAtLeast(result, cr);
			}
		}
		// add global concepts from at most restrictions
		for (Concept c : globalConcepts) {
			for (Iterator<Individual> i = result.individualIterator(); i
					.hasNext();) {
				Individual indv = i.next();
				result.add(new ConceptAssertion(c, indv.getName()));
			}
		}
		return result;
	}

	private void addAtLeast(ABox result, CardinalityRestriction cr)
			throws UnsatisfiableException {
		List<String> indvNames = new ArrayList<String>();
		for (int i = 1; i <= cr.getNo(); i++) {
			String newIndvName = IndividualNameManager.getInstance()
					.generateIndividualName();
			result.add(new ConceptAssertion(cr.getConcept(), newIndvName));
			result.add(new ConceptAssertion(new Nominal(newIndvName),
					newIndvName));
			indvNames.add(newIndvName);
		}
		// assert inequalities
		for (String indvName1 : indvNames) {
			for (String indvName2 : indvNames) {
				if (indvName1 != indvName2) {
					Nominal nom1 = new Nominal(indvName1);
					Nominal nom2 = new Nominal(indvName2);
					result.add(new ConceptAssertion(nom1.toggleNegated(),
							indvName2));
					result.add(new ConceptAssertion(nom2.toggleNegated(),
							indvName1));
				}
			}
		}
	}

	private Concept addAtMost(ABox result, CardinalityRestriction cr)
			throws UnsatisfiableException {
		Concept globalConcept = new BooleanConcept();
		((BooleanConcept) globalConcept).setConstructor(Constructor.UNION);
		((BooleanConcept) globalConcept).setLhs(cr.getConcept().copy()
				.toggleNegated());
		BooleanConcept currentDisjunction = (BooleanConcept) globalConcept;
		for (int i = 1; i <= cr.getNo(); i++) {
			String newIndvName = IndividualNameManager.getInstance()
					.generateIndividualName();
			Nominal nom = new Nominal(newIndvName);
			result.add(new ConceptAssertion(nom, newIndvName));
			if (i == cr.getNo()) {
				currentDisjunction.setRhs(nom);
			} else {
				BooleanConcept disjunction = new BooleanConcept();
				disjunction.setConstructor(Constructor.UNION);
				disjunction.setLhs(nom);
				currentDisjunction.setRhs(disjunction);
				currentDisjunction = disjunction;
			}
		}
		if (cr.getNo() == 0) {
			globalConcept = cr.getConcept().copy().toggleNegated();
		}
		return globalConcept;
	}
}
